T:Type, eq:EqDecider(T), f:(TT), x:T. retraction(T;f)  (f**(f(x)) = f**(x)  T) 

latex

Definitions

Type, t  T, s = t, x:AB(x), x:A. B(x), EqDecider(T), retraction(T;f), strong-subtype(A;B), P  Q, A, left + right, P  Q, Dec(P), x:A  B(x), x:A. B(x), b | a, a ~ b, a  b, a <p b, a < b, A c B, x f y, xL. P(x), (xL.P(x)), r  s, r < s, q-rel(r;x), Outcome, f(a), eqof(d), b, True, T, , f**(x), P & Q, P  Q, P  Q, False, ff, , b, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, , =, a < b, =, =, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), p  q, p  q, p q, tt, , Unit

Lemmas

eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, iff wf, rev implies wf, assert wf, deq property, fix wf, squash wf, decidable assert, eqof wf, retraction wf, deq wf